T:Type, j:, l:T List. 0<j  j||l||  ((firstn(j-1;l) @ [l[j-1]]) ~ firstn(j;l)) 

latex

Definitions	if b t else f fi, Unit, , b, b, P  Q, P & Q, T, P  Q, True, S  T, Top, l[i], ij, i<j, hd(l), tl(l), Dec(P), P  Q, SQType(T), {T}, ij, , A, False, as @ bs, firstn(n;as), ||as||, Prop, t  T, x:A. B(x), P  Q, AB
Lemmas	length wf1, le wf, nat wf, nat properties, ge wf, decidable int equal, list decomp, top wf, tl wf, first0, length tl, true wf, squash wf, bnot wf, assert wf, le int wf, lt int wf, assert of le int, bnot of lt int, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, bool wf, bnot of le int